| Definitions | t  T,  x:A. B(x), <a,b>, {T}, P   Q, SQType(T), es-M(es), Msg, kind(a), Knd, x:A  B(x), P  Q, x:A B(x), P & Q, P Q, False, P  Q, Void, left+right, IdLnkDeq, IdLnk, false , a = b, (x l), deq-member(eq;x;L), Type, Prop, p q, IdDeq, Id, kind(e), es_info(es), E,  x.A(x),  , product-deq(A;B;a;b), loc(e), E, e@i. P(e), A & B, f(x), x dom(f), mk-ma, x : v, f(x)?z, z != f(x) P(a;z), k sends only on links in L, M.ds(x), M.bframe(k sends on l), M(i), @i: k sends only links in L, M.aframe(k affects x), M.sframe(k sends <l,tg>), M.frame(k affects x), M.send(k;l;s;v;ms;i), M.ef(k,x,s,v,w), M.pre(a,s,v), M.init(x,v), PossibleWorld(D;w), es-oaxioms(es), es_val(es), es-pred?(es), es-eq(es), sends(l;e), ES(the_w), kind(e), FairFifo, World, D realizes2 es.P(es), {x:A| B(x) }, (Msg on l), es is an event system of D, ES, nil, S  T, x. t(x), D realizes es. P(es), loc(e), s ~ t, time(e), m(i;t), onlnk(l;mss), w_sends(e;l), Msg, type List, s = t, a(i;t), isnull(a),  b,  A |